COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ekl.206[f81,jmc]		ekl problems for cs206
C00004 ENDMK
C⊗;
ekl.206[f81,jmc]		ekl problems for cs206

	The following problems are to be done in EKL.  You may use
the axioms for lisp at lots in the file xxx.

	1. Define copy(u) by the ekl declarations and axioms
(decl copy |ground→ground| constant)

(axiom |∀u.copy(u) = if null(u) then nnil else cons(car(u),copy(cdr(u)))|)

	a. Prove that copy is total, i.e. that ∀u.listp(copy(u)).

	b. Prove ∀u.copy(u) = u.

	2. Define the union of two lists by the ekl axiom

(declare union |ground→ground| constant)

(axiom |∀u v.union(u,v) = if null(u) then v
           else if member(car(u),v) then union(cdr(u),v)
           else cons(car(u),union(cdr(u),v))|)

Prove that
	a. union is total, i.e. takes lists into lists.

	b. union is associative, i.e. union(u,union(v,w)) = union(union(u,v),w).

	3. Define

(defun flat (x u) (cond
		   ((atom x) (cons x u))
		   (t (flat (car x) (flat (cdr x) u)))))

and

(defun fringe (x) (cond
		   ((atom x) (cons x nil))
		   (t (append (fringe (car x)) (fringe (cdr x))))))

Translate these into appropriate ekl declarations and axioms and
prove

	∀x u.flat(x,u) = append(fringe(x),u)